package controller.solver;

import java.io.BufferedReader;
import java.io.File;
import java.io.IOException;
import java.io.InputStreamReader;
import java.util.Scanner;

import model.solver.MiniSatParameter;
import model.solver.ParameterValue;
import model.solver.SolverParameter;
import model.solver.SolverResult;
import model.solver.SolverResultStatus;

/**
 * This class is a implementation of Solver for Minisat
 * 
 * @author stephane
 *
 */
public class MiniSat extends Solver {

	public static final String EXEC = "minisat";
	public static final String DESCRIPTION = "Result of the minisat execution";
		
	public static final String RESTARTS_TOKEN = "restarts";
	public static final String DECISIONS_TOKEN = "decisions: ";
	public static final String CONFLICTS_TOKEN = "conflicts: ";
	public static final String PROPAGATIONS_TOKEN = "propagations";
	public static final String CINF_LITTERALS_TOKEN = "conflict literals";
	public static final String MEMORY_TOKEN = "Memory used";
	
	
	//public static final int DEFAULT_RETURN_VALUE = 0; 
	public static final int RETURN_UNSATISFIABLE = 20;
	public static final int RETURN_SATISFIABLE = 0;
	
	private MiniSatParameter param;
	
	public MiniSat(File directory) throws IOException {
		if(!directory.isDirectory() || ! new File(directory, EXEC).isFile())
			throw new IllegalArgumentException();
		
		param = new MiniSatParameter();
		
		try {
			path = directory.getCanonicalPath() + File.separator + EXEC;
		} catch (IOException e) {
			e.printStackTrace();
			throw new IOException();
		}
	}

	public MiniSatParameter getMiniSatParameter() {
		return param;
	}

	@Override
	public boolean checkParameter() {
		return param.basicCheck();
	}

	@Override
	public SolverParameter getSolverParameter() {
		return param;
	}
	
	@Override
	public String[] getCommandLine(String cnfFile) {
		// TODO ajouter les autre arg
		
		String[] tab = new String[2 + param.getCommandLineNbParameterSup()];
		
		//bash
		tab[0] = path;
		//satellite
		if(param.isPre())
			tab[1] = "-pre=once";
		else
			tab[1] = "-pre=none";
		
		int nb = 2;
		//asym
		if(param.getAsymm() != ParameterValue.NOT_USED)
			tab[nb++] = "-asymm="+param.getAsymm().getVal();
		//rcheck
		if(param.getRcheck() != ParameterValue.NOT_USED)
			tab[nb++] = "-rcheck="+param.getRcheck().getVal();
		//grow
		if(param.getGrow() != MiniSatParameter.NOT_USED)
			tab[nb++] = "-grow="+param.getGrow();
		//polarity
		if(param.getPolarityMode() != ParameterValue.NOT_USED)
			tab[nb++] = "-polarity-mode="+param.getPolarityMode().getVal();
		//decay
		if(param.getDecay() != MiniSatParameter.NOT_USED)
			tab[nb++] = "-decay="+param.getDecay();
		//rnd freq
		if(param.getRndfreq() != MiniSatParameter.NOT_USED)
			tab[nb++] = "-rnd-freq="+param.getRndfreq();
		//rnd verbosity
		if(param.getVerbosity() != MiniSatParameter.NOT_USED)
			tab[nb++] = "-verbosity="+param.getVerbosity();
		
		//stdin
		tab[nb] = cnfFile;//correctFormatForLinux(cnfFile);
			
		return tab;
	}

	@Override
	public boolean hasTimeout() {
		return false;
	}

	@Override
	public SolverResult runSolver(String[] cmd) {
		SolverResult res = new SolverResult(); 
		
		BufferedReader input = null;
		BufferedReader inerr = null;
		try{//lance le processus
			res.setBegin(System.currentTimeMillis());
			setRunning(true);
			
			process = Runtime.getRuntime().exec(cmd);

			String line;
			input = new BufferedReader (new InputStreamReader(process.getInputStream()));
			inerr = new BufferedReader (new InputStreamReader(process.getErrorStream()));
			
			while ((line = input.readLine()) != null) 
			{ //verifie les stdin
				System.out.println(line);
				res.addStdin(line+"\n");
			}
			while ((line = inerr.readLine()) != null) 
			{ //verifie les stderr
				//System.out.println(line);
				res.addStderr(line+"\n");
			}
		}
		catch(IOException e){
			//e.printStackTrace();
			res.setStatus(SolverResultStatus.PROBLEM);
			if(process != null)
				process.destroy();
		}
		finally{
			try{
				if(input != null)
					input.close();
				if(inerr != null)
					inerr.close();
				if(process != null)
					res.setExitVal(process.waitFor());
			}
			catch(Exception e){
				//e.printStackTrace();
				res.setStatus(SolverResultStatus.PROBLEM);
			}
			finally{
				setRunning(false);
			}
		}
		//terminer
		res.setEnd(System.currentTimeMillis());

		System.out.println("val de retour"+res.getExitVal());
		
		//s'occupe du status
		if(hasBeenStop()) //cas timeout
			res.setStatus(SolverResultStatus.TIMEOUT_REACHED);
		else
			if(res.getStatus() == SolverResultStatus.PROBLEM)
				switch(res.getExitVal()){
				case RETURN_UNSATISFIABLE : res.setStatus(SolverResultStatus.UNSATISFIABLE) ; break ;
				case RETURN_SATISFIABLE : 
					res.setStatus(SolverResultStatus.SATISFIABLE) ; 
					setLastResult(res);
					break ;
				
				default : res.setStatus(SolverResultStatus.PROBLEM) ; 
				}
					
		//dernier details
		res.setDescription(DESCRIPTION);
		
		return res;
	}

	private void setLastResult(SolverResult res){
		int index = res.getStderr().indexOf(RESTARTS_TOKEN);
		
		if(index == -1)
			return;
		
		//recupere la chaine de puis le token
		String out = res.getStderr().substring(index);
		//	String pattern = "\\s*" + RESTARTS_TOKEN + "\\s*:\n\\s*" + CONFLICTS_TOKEN + "\\s*:\n\\s*"	
		Scanner scan = new Scanner(out);
		//restarts
		for(int i = 2 ; i > 0 ; i--)
			scan.next();
		res.setRestarts(scan.nextInt());
		//conflicts
		for(int i = 2 ; i > 0 ; i--)
			scan.next();
		res.setConflics(scan.nextInt());
		//decisions
		for(int i = 4 ; i > 0 ; i--)
			scan.next();
		res.setDecisions(scan.nextInt());
		//propagations
		for(int i = 7 ; i > 0 ; i--)
			scan.next();
		res.setPropagations(scan.nextInt());
		//conflic literal
		for(int i = 5 ; i > 0 ; i--)
			scan.next();
		res.setConflicLiterals(scan.nextInt());
		//memory used
		for(int i = 7 ; i > 0 ; i--)
			scan.next();
		res.setMemoryUsed(scan.next() + " " + scan.next());
		
		
	}

	

	
}
